proposition: Lemma mult_eq_zero : forall a b : nat, a * b =N= 0 -> a =N= 0 |_| b =N= 0.
proof: Proof. intros [|a] [|b];auto. - intros _;right;reflexivity. - simpl_nat. intros E. destruct (S_neq_0 _ E). 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