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