proposition: Lemma rati_neg x (f:= rat_iterator) (T:= fun x => BQinv (BQopp x)) (y := f x) : inc x BQps -> f (T y) = T x.
proof: Proof. move => xp; congr BQinv. have xq:=(BQps_sBQ xp). have yqps: inc y BQps by apply: (rati_pos (BQps_sBQp xp)). have yq: ratp y by apply:BQps_sBQ. have h0:= (ZS_floor xq); have h1:=(ZSp ZS2 h0). move: (BQ_of_Z_iQ h0); set t := (BQ_of_Z (BQfloor x)) => tq. have t2q:=(QSdouble tq). have d1q: inc (\1q +q BQdouble t) BQ by apply:(QSs QS1). have: T y = BQopp (\1q +q (BQdouble (BQ_of_Z (BQfloor x))) -q x). rewrite /T (BQinv_opp yq); congr BQopp; apply: (BQinv_K (QS_diff d1q xq)). rewrite (BQoppB d1q xq) => sa. have hb:= (QSo (QSs QS1 tq)). have ha: (exists2 c, inc c BZ & (BQopp (\1q +q BQdouble t)) = BQ_of_Z c). exists (BZopp (\1z +z (\2z *z (BQfloor x)))). apply:ZSo; apply:(ZSs ZS1 h1). by rewrite - BQopp_cZ - (BQsum_cZ ZS1 h1) -(BQprod_cZ ZS2 h0). move:(f_equal BQ_of_Z (f_equal BQfloor sa)). rewrite(BQfloor_spec_sum xq ha) => ->. rewrite - (BQdouble_p tq) (BQsumA QS1 tq tq) (BQoppD (QSs QS1 tq) tq). rewrite (BQsumA tq hb (QSo tq)) -/ (_ -q _) (BQdiff_sum tq hb) sa. suff: (\1q +q BQdouble (BQopp (\1q +q t))) = BQopp(\1q +q BQdouble t). move => ->; rewrite (BQdiff_diff (QSo d1q) xq d1q) BQsumC /BQdiff. by rewrite (BQsumC _ (BQopp x)) -/(_ -q _) (BQsum_diff d1q (QSo xq)). rewrite - {1} (BQopp_K QS1) (BQdouble_opp (QSs QS1 tq)). rewrite -(BQoppD (QSo QS1) (QSdouble (QSs QS1 tq)))(BQdoubleD QS1 tq). rewrite (BQsumA (QSo QS1) (QSdouble QS1) (QSdouble tq)). rewrite (BQsumC (BQopp \1q)) -/(_ -q _) - (BQdouble_p QS1). by rewrite (BQdiff_sum QS1 QS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)