Require Omega.

Section TP4.

(*** Exercice 1 ***)

Definition monZ := prod nat nat.

Definition eq (a:monZ) (b:monZ) : Prop := (* ... *).

Definition zero := (0,0).

Theorem not_injective : eq zero (* ... *).
Proof.
(* ... *)
Qed.

Definition add (a:monZ) (b:monZ) : monZ := (* ... *).

Require Import Omega.

Theorem add_compat_eq : forall x1 x2 y1 y2, eq x1 x2 -> eq y1 y2 -> eq (add x1 y1) (add x2 y2).
Proof.
(* ... *)
Qed.


Definition op (a:monZ) : monZ := (* ... *).

Theorem op_compat_eq : (* ... *).
Proof.
(* ... *)
Qed.

Theorem add_op : forall x, eq zero (add x (op x)).
Proof.
(* ... *)
Qed.



Definition leq (a:monZ) (b:monZ) : Prop := (*... *).

Theorem reflexif : forall x y, eq x y -> leq x y.
Proof.
(* ... *)
Qed.

Theorem transitif: forall x y z, (* ... *).
Proof.
(* ... *)
Qed.

Theorem antisym : forall x y,(* ... *).
Proof.
(* ... *)
Qed.



(*** Exercice 2 ***)

Inductive plus : (* ... *)


Lemma plus_symm : (* ... *)


Lemma plus_tot :(* ... *)



Theorem plus_plus : forall x y z, plus x y z -> x+y=z.
Proof.
(* ... *)
Qed.

Lemma plus_fonc : forall x y z1 z2, plus x y z1 -> plus x y z2 -> z1 = z2. 
Proof.
(* ... *)
Qed.

End TP4.