proposition: Lemma A_mult_assoc m n p : Amult m (Amult n p) = Amult (Amult m n) p.
proof: Proof. unfold Amult. destruct m; destruct n; destruct p; trivial. rewrite Nat.add_assoc. trivial. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ)