proposition: Lemma natlehmultnatdiv (n m : nat) (is : m ≠ 0) : natdiv n m * m ≤ n.
proof: Proof. intros. set (e := natdivremrule n m is). set (int := (natdiv n m) * m). rewrite e. apply natlehmplusnm. Defined.
imports: UniMath.Foundations.Sets