proposition: Lemma sub_Some p q r : p - q = Some r ↔ p = q + r.
proof: Proof. destruct p as [p Hp], q as [q Hq], r as [r Hr]. unfold sub, add; simpl; rewrite <-Qp.to_Qc_inj_iff; simpl. split. - intros; simplify_option_eq. unfold Qcminus. by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. - intros ->. unfold Qcminus. rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc. rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done]. f_equal. by apply Qp.to_Qc_inj_iff. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)