proposition: Lemma quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
proof: Proof. intros [??] ?. destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |]. destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |]. split; [apply Z.quot_pos; lia|]. trans x; auto. apply Z.quot_lt; lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)