proposition: Lemma not_lt_0 : forall a, ~ (a < 0).
proof: Proof. intros a E. apply le_exists in E. destruct E as [k E]. apply natpaths_symm,plus_eq_zero in E. apply (S_neq_0 _ (snd E)). 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