proposition: Lemma BQfloor_spec_sum a b: ratp a -> (exists2 c, inc c BZ & b = BQ_of_Z c) -> BQ_of_Z (BQfloor (a +q b)) = BQ_of_Z (BQfloor a) +q b.
proof: Proof. move => aq [c cz ->]. have faz:= (ZS_floor aq). have cq:= (BQ_of_Z_iQ cz). have sz:= (ZSs faz cz). rewrite (BQsum_cZ faz cz); congr BQ_of_Z. move: (BQ_floorp aq); set fa := BQfloor a; move => [sa sb]. symmetry; apply: (BQ_floorp2 (QSs aq cq) sz); split. by rewrite - BQsum_cZ; move/(BQsum_le2r (proj31 sa) aq cq): sa. rewrite - (BQsum_cZ faz cz) (BQsumC _ \1q) (BQsumA QS1 (proj31 sa) cq). by rewrite (BQsumC \1q); apply/(BQsum_lt2r aq (proj32_1 sb) cq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)