proposition: Theorem mod_lt a b : b<>0 -> a mod b < b.
proof: Proof. destruct b as [ |b]. { now destruct 1. } destruct a as [ |a]. { reflexivity. } unfold modulo. simpl. apply pos_div_eucl_remainder. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties