proposition: Lemma nonzero_gt_0 : forall a, ~ (a =N= 0) -> 0 < a.
proof: Proof. intros [|a] E. - destruct E;split. - apply S_gt_0. 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