1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid".
17 include "NPlus/monoid.ma".
18 include "Zah/defs.ma".
20 theorem nplus_total: \forall p,q. \exists r. p + q == r.
21 intros 2. elim q; clear q;
25 theorem zeq_intro: \forall z1,z2.
26 (\forall n.((\fst z1) + (\snd z2) == n) \to ((\fst z2) + (\snd z1) == n)) \to
27 (\forall n.((\fst z2) + (\snd z1) == n) \to ((\fst z1) + (\snd z2) == n)) \to
29 unfold ZEq. intros. apply iff_intro; intros; auto.
32 theorem zeq_refl: \forall z. z = z.
33 unfold ZEq. intros. auto.
36 theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
37 unfold ZEq. intros. lapply linear (H n). auto.
40 theorem zeq_trans: \forall z1,z2. z1 = z2 \to
41 \forall z3. z2 = z3 \to z1 = z3.
43 lapply (nplus_total (\snd z2) (\fst z2)). decompose.
47 apply iff_intro; intros;
48 [ lapply (nplus_total (\fst z1) (\snd z3)). decompose
54 lapply (nplus_total (\snd z2) (\fst z2)). decompose.
55 lapply (nplus_total n a). decompose.
56 lapply linear (H a1). lapply linear (H1 a1). decompose.