proposition: Lemma eqb_eq n m : eqb n m = true <-> n=m.
proof: Proof. destruct n as [|n], m as [|m]; simpl; try easy'. rewrite Pos.eqb_eq. split; intro H. - now subst. - now destr_eq H. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties