proposition: Lemma sub_succ_r n m : n - succ m = pred (n - m).
proof: Proof. unfold sub, succ, pred. now rewrite opp_add_distr, add_assoc. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass