proposition: Lemma nat_le_lt_trans : forall a b c : nat, a <= b -> b < c -> a < c.
proof: 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.
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