(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/decl".
+
include "nat/times.ma".
include "nat/orders.ma".
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-conclude (S n) = (S m) by (eq_f ? ? ? ? ? H).
+conclude (S n) = (S m) by H.
= (S p) by K.
- = n by (sym_eq ? ? ? L)
+ = n by L
done.
qed.
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-conclude (S n) = (S m) by _.
- = (S p) by _.
- = n by _
+conclude (S n) = (S m).
+ = (S p).
+ = n
done.
qed.