proposition: Lemma size_lift n p : size (lift n p) = n + size p.
proof: Proof. Proof (size_ncons n C.zero p). Definition mul_mixed (u : U) (a : C.T) (p : T) := @foldr C.T T (fun x acc => (C.mul u a x) :: acc) [::] p. Definition div_mixed_r (u : U) (p : T) (b : C.T) := @foldr C.T T (fun x acc => (C.div u x b) :: acc) [::] p. Lemma size_mul_mixed u a p : size (mul_mixed u a p) = size p. Proof. by elim: p => [//|x p IHp]; rewrite /= IHp. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec