proposition: Theorem plus_rearrange : forall n m p q : nat, (n + m) + (p + q) = (m + n) + (p + q).
proof: Proof. MProof. intros n m p q. assert (H : n + m = m + n). - rewrite -> PeanoNat.Nat.add_comm &> reflexivity. - rewrite -> H &> reflexivity. Qed.
imports: Mtac2.Mtac2 Lists.List