proposition: Lemma mul_split_l n x1 x2 y1 y2 : x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
proof: Proof. intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |]. revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)