proposition: Lemma BQabs_prop2 x y: ratp x -> ratp y -> (BQabs x <q y <-> (BQopp y <q x /\ x <q y)).
proof: Proof. move => xq yq. case /BQ_i0P: (xq) => xp. rewrite (BQabs_negs xp); move: (qlt_oppP (QSo xq) yq);rewrite (BQopp_K xq). move => h;apply:(iff_trans (iff_sym h)); split; last by move => []. move => h1; split => //. move:(BQms_sBQm xp) => xp'. move:(qle_par3 (BQopp_negative2 xp') xp') => h2. move/h: h1 => h3; BQo_tac. rewrite (BQabs_pos xp); split; last by move => []. move => lxy; split => //; rewrite - (BQopp_K xq); apply: qlt_opp. have h: BQopp x <=q x by apply:(qle_par3 xp (BQopp_positive2 xp)). BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)