proposition: Lemma mod_pos_bound a b : 0 < b -> 0 <= a mod b < b.
proof: Proof. destruct b as [|b|b]; try easy; intros _. destruct a as [|a|a]; unfold modulo, div_eucl. - now split. - now apply pos_div_eucl_bound. - generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. + now split. + split. * unfold le. now rewrite compare_antisym, <- compare_sub, <- compare_antisym, Hr'. * unfold lt in *; simpl in *. rewrite pos_sub_gt by trivial. simpl. now apply Pos.sub_decr. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass