proposition: Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
proof: Proof. destruct n. - trivial. - simpl pred. rewrite pred_succ. apply of_nat_succ. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef