proposition: Fact Div_Mod x y : x = S y * Div x (S y) + Mod x (S y).
proof: Proof. induction x as [x IH] using lt_wf_ind. simp Div Mod. Opaque mult. destruct (le_lt_dec _ _) as [H|H]; cbn. - assert (x - S y < x) as IH1%IH by lia. lia. - lia. Qed.
imports: Coq(Arith Lia) Equations(Equations)