proposition: Lemma natdivleh ( a b k : nat ) ( f : ( a * k )%nat = b ) : natleh a b ⨿ ( b = 0%nat ).
proof: Proof. intros. destruct k. - rewrite natmultcomm in f. simpl in f. apply ii2. apply pathsinv0. assumption. - rewrite natmultcomm in f. simpl in f. apply ii1. apply natlehdecomp. intro P. intro g. apply g. split with ( k * a )%nat. rewrite natpluscomm. assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids