(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/decl".
+set "baseuri" "cic:/matita/tests/decl".
include "nat/times.ma".
include "nat/orders.ma".
assume P: Prop.
suppose (P ∧ ∃m:nat.m ≠ m) (H).
by H we have P (H1) and (∃x:nat.x≠x) (H2).
- (*BUG:
by H2 let q:nat such that (q ≠ q) (Ineq).
- *)
- (* the next line is wrong, but for the moment it does the job *)
- by H2 let q:nat such that False (Ineq).
by I done.
qed.
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
+conclude (S n) = (S m) by (eq_f ? ? ? ? ? H).
= (S p) by K.
= n by (sym_eq ? ? ? L)
done.
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-obtain (S n) = (S m) by _.
+conclude (S n) = (S m) by _.
= (S p) by _.
= n by _
done.
destruct absurd.
by final
done.
-qed.
\ No newline at end of file
+qed.