proposition: Lemma modNat_mult : forall x (p : posnat), modNat (x * p) p = 0.
proof: Proof. induction x; intuition; simpl in *. rewrite modNat_plus. rewrite modNat_arg_eq. rewrite Nat.add_0_l. eauto. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat