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