Module prac3 Import basic; Inductive [Leq : Nat -> Nat -> Set] Constructors [le0 : {n:Nat}Leq ze n] [leS : {m,n|Nat}(Leq m n)->(Leq (su m) (su n))]; Goal {n:Nat}(Leq n n); Refine ind ([n:Nat]Leq n n); Refine le0; Intros; Refine leS; Immed; Save refl_leq; Goal {n:Nat}(Leq n ze)->(Id n ze); Save leq_inv0; Goal {m,n|Nat}(Leq (su m) (su n))->(Leq m n); Save leq_invS; Goal {i,j,k|Nat}(Leq i j)->(Leq j k)->(Leq i k); Save trans_leq; Goal {m,n|Nat}(Leq m n)->(Leq n m)->(Id m n); Save antisym; Goal {m,n:Nat}Plus (Leq m n) (Leq n m); Save dec_Leq;