proposition: Lemma pred_div2_up p : Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p).
proof: Proof. destruct p as [p|p| ]; trivial. - simpl. apply Pos.pred_N_succ. - destruct p; simpl; trivial. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties