proposition: Lemma shiftr_succ_r a n : shiftr a (succ n) = div2 (shiftr a n).
proof: Proof. destruct n; simpl; trivial. apply Pos.iter_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties