proposition: Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y.
proof: Proof. split; intros. - by apply Qcplus_le_compat. - replace x with ((0 - z) + (z + x)) by ring. replace y with ((0 - z) + (z + y)) by ring. by apply Qcplus_le_compat. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)