Simulating elim with apply
Redo the following proof, using the tactic
apply instead of elim:
Theorem lt_le : forall n p:nat, n < p \arrow{} n {\coqle} p.
Proof.
intros n p H; elim H; repeat constructor; assumption.
Qed.
Solution
This file
Going home
Pierre Castéran