proposition: Lemma nat_lt_not_le : forall a b : nat, a < b -> ~ (b <= a).
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness