proposition: Lemma Qcle_shift_minus_l : forall q₁ q₂ q₃, q₁ + q₃ <= q₂ -> q₁ <= q₂ - q₃.
proof: Proof. intros q₁ q₂ q₃ Hle. replace q₁ with (q₁ + q₃ - q₃) by ring. apply Qcminus_le_compat. easy. reflexivity. Qed.
imports: Qfield Qreduction Qcanon