proposition: Lemma add_succ_l n m : succ n + m = succ (n + m).
proof: Proof. unfold succ. now rewrite 2 (add_comm _ 1), add_assoc. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass