proposition: Lemma A_plus_comm m n : Aplus m n = Aplus n m.
proof: Proof. unfold Aplus. destruct m; destruct n; trivial. rewrite Z.max_comm. 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)