proposition: Lemma pred_succ n : pred (succ n) = n.
proof: Proof. unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass