proposition: Lemma BQabs_prop3 x y e: ratp x -> ratp y -> ratp e -> (BQabs (x -q y) <=q e <-> y -q e <=q x /\ x <=q y +q e).
proof: Proof. move => xr yr er. have Ha: BQopp e <=q x -q y <-> y -q e <=q x. rewrite - (BQoppB yr xr). exact (iff_trans (qle_oppP (QS_diff yr xr) er) (BQdiff_le1P yr xr er)). have Hb: x -q y <=q e <-> x <=q y +q e. move:(BQsum_le2r xr (QSs yr er) (QSo yr)). by rewrite -/(_ -q _) -/(_ -q _) (BQdiff_sum yr er). move:(BQabs_prop1 (QS_diff xr yr) er) => H. split; first by move/H => [/Ha ha /Hb hb]. by move => [/Ha ha /Hb hb]; apply/H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)