forall a b : nat, a < b -> ~ (b <= a). Proof. intros a b E1 E2. apply le_exists in E1;apply le_exists in E2. destruct E1 as [k1 E1], E2 as [k2 E2]. apply (S_neq_0 (k1 + k2)). apply (left_cancellation (+) a). fold natpaths. rewrite add_0_r. rewrite E1 in E2. rewrite add_S_r;rewrite !add_S_r in E2. rewrite (add_assoc a), (add_comm a), <-(add_assoc k1), (add_comm a). rewrite (add_assoc k1), (add_comm k1), <-(add_assoc k2). apply natpaths_symm,E2. Qed.
Require Import