The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Yes, use of "assert" or "cut" tactic can be useful. I will not provide the proof script, as it is quite easy. If you still find it hard, you should really read some documentation (Software Foundations, or Certified Programming with Dependant Types, for instance). The Coq reference manual is also a valuable reference.

2014-08-20 14:53 GMT+02:00 .... <nixiejun AT 163.com>:

Dear Coq users:

    Here I meet a question.

    1 subgoals
P : Prop
Q : Prop
R : Prop
H : P -> Q
______________________________________(1/1)
Q \/ R

    

    Is it possible to use H:P->Q to transform subgoal Q\/R to P\/R. 

--
.../Sedrikov\...