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.