proposition: Lemma cross_split a b c d : a + b = c + d → ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d.
proof: Proof. intros H. revert a b c d H. cut (∀ a b c d : Qp, a < c → a + b = c + d → ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp. { intros help a b c d Habcd. destruct (lt_ge_cases a c) as [?|[?| ->]%le_lteq]. - auto. - destruct (help c d a b); [done..|]. naive_solver. - apply (inj (add a)) in Habcd as ->. destruct (lower_bound a d) as (q&a'&d'&->&->). exists a', q, q, d'. repeat split; done || by rewrite (comm_L add). } intros a b c d [e ->]%lt_sum. rewrite <-(assoc_L _). intros ->%(inj (add a)). destruct (lower_bound a d) as (q&a'&d'&->&->). eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L add)|..|done]. - by rewrite (assoc_L _), (comm_L add e). - by rewrite (assoc_L _), (comm_L add a'). Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)