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