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. destruct (le_dec n n0). rewrite !max_l. trivial. auto with arith. trivial. rewrite !max_r. trivial. auto with arith. trivial. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ)