forall a b c : nat, a <= b -> b < c -> a < c. Proof. intros a b c E1 E2. apply le_exists in E1;apply le_exists in E2. destruct E1 as [k1 E1],E2 as [k2 E2];rewrite E2,E1. rewrite add_S_r,add_assoc. apply le_S_S,le_plus. Qed.
Require Import