proposition: Theorem add_succ_l n m : succ n + m = succ (n + m).
proof: Proof. destruct n, m; unfold succ, add; now rewrite ?Pos.add_1_l, ?Pos.add_succ_l. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties