proposition: Lemma nat_not_lt_le : forall a b, ~ (a < b) -> b <= a.
proof: Proof. intros ?? E. destruct (le_lt_dec b a);auto. destruct E;auto. 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