proposition: Lemma succ_double_lt_mono n m : n < m -> succ_double n < succ_double m.
proof: Proof. destruct n as [|n], m as [|m]; intros H; try easy. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties