proposition: Lemma succ_double_lt n m : n<m -> succ_double n < double m.
proof: Proof. destruct n as [|n], m as [|m]; intros H; try easy. unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties