proposition: Lemma lt_strong_cotrans : forall a b : nat, a < b -> forall c, a < c |_| c < b.
proof: Proof. intros a b E1 c. destruct (le_lt_dec c a) as [E2|E2]. - right. apply nat_le_lt_trans with a;trivial. - left;trivial. Defined.
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