(* Dwie inne definicje le i troche lematow o le*)

Require Import Omega.

(*Pierwsza inna definicja le*)
				    
Inductive le_diff (n: nat)(m:nat) : Prop :=
| le_d : forall x:nat, x+n=m -> le_diff n m.

(*Udowodnij rownowaznosc le i le_diff*)

Lemma le_le_diff: forall m n, le m n ->  le_diff m n.


Lemma le_diff_le: forall m n, le_diff m n ->  le m n.


(*Druga inna definicja le*)

Inductive le': nat->nat->Prop :=
| le'_0_p: forall p:nat, le' 0 p
| le'_Sn_Sp : forall n p:nat, le' n p -> le' (S n) (S p).


(*Udowodnij rownowaznosc le i le'*)

Lemma le_le': forall m n, le m n ->  le' m n.


Lemma le'_le: forall m n, le' m n ->  le m n.


(* Troche lematow o le

   w dowodach prosze nie uzywac taktyki omega 
*)
				   
  
Print le_trans.

					   
					   
Lemma le_plus_r: forall m n p, m<=n -> m+p<=n+p.


Lemma le_plus_l: forall m n p, m<=n -> p+m<=p+n.


Lemma le_plus_2: forall m n p q, m<=n -> p<=q -> m+p<=n+q.



					   
Lemma mult_le_l: forall m n p, n <= p -> m*n <= m*p.


Lemma mult_le_r: forall m n p, n <= p -> n*m <= p*m.


Lemma le_mult_2: forall a b c d, a<=c -> b<=d -> a*b <= c*d.