proposition: Lemma lt_sum p q : p < q ↔ ∃ r, q = p + r.
proof: Proof. destruct p as [p Hp], q as [q Hq]. rewrite to_Qc_inj_lt; simpl. split. - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt). apply Qp.to_Qc_inj_iff; simpl. unfold Qcminus. by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. - intros [[r ?] ?%Qp.to_Qc_inj_iff]; simplify_eq/=. rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)