proposition: Lemma Q4 : forall n, v n = 1 / 6 * (1 + 5 * (94 / 100) ^ n) * v 0 + 1 / 6 * (1 - (94 / 100) ^ n) * c 0.
proof: Proof. intros n. assert (X n = scal (pow_n A n) (X 0)). elim: n => [ | n IH] /=. by rewrite scal_one. rewrite -scal_assoc -IH. by apply Q2. assert (pow_n D n = [[1,0], [0,(94 / 100)^n]]). elim: (n) => [ | m IH] //=. rewrite IH. apply (coeff_mat_ext_aux 0 0) => i j Hi Hj. rewrite coeff_mat_bij => //=. rewrite /plus /mult /= /coeff_mat /=. (destruct i as [ | i] ; destruct j as [ | j] ; rewrite /zero /one /=) ; (try (destruct i as [ | i]) ; try (destruct j as [ | j]) ; rewrite /zero /one /= ; try field) ; rewrite sum_Sn sum_O /= /plus /= ; field. rewrite Q3c H0 in H. apply (proj1 (coeff_mat_ext 0 _ _)) with (i := O) (j := O) in H. rewrite {1}/coeff_mat /= in H. rewrite H ; repeat (rewrite !/coeff_mat /=). rewrite !sum_Sn !sum_O /= /plus /mult /= ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Hierarchy PSeries Rbar Lim_seq)