proposition: Lemma add_comm n m : n + m = m + n.
proof: Proof. destruct n, m; simpl; trivial; now rewrite Pos.add_comm. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass