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