proposition: Lemma A_mult_plus_distr m n p : Amult (Aplus m n) p = Aplus (Amult m p) (Amult n p).
proof: Proof. unfold Amult, Aplus. destruct m; destruct n; destruct p; trivial. rewrite Zplus_max_distr_r. destruct (Zmax_irreducible_inf z z0); rewrite e; refl. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)