proposition: Lemma lt_succ_r n m : n < succ m <-> n<=m.
proof: Proof. destruct n as [|p], m as [|q]; simpl; try easy'. - split. + now destruct p. + now destruct 1. - apply Pos.lt_succ_r. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties