proposition: Lemma Q3a : mult P P' = Mone /\ mult P' P = Mone.
proof: Proof. split. apply (coeff_mat_ext_aux 0 0) => i j Hi Hj. rewrite coeff_mat_bij => //. rewrite /coeff_mat /= /mult /plus /=. (destruct i as [ | i] ; destruct j as [ | j] ; rewrite /zero /= ; try field) ; (try (destruct i as [ | i]) ; try (destruct j as [ | j]) ; rewrite /zero /one /= ; try field) ; rewrite sum_Sn sum_O /= /plus /= ; field. apply (coeff_mat_ext_aux 0 0) => i j Hi Hj. rewrite coeff_mat_bij => //. rewrite /coeff_mat /= /mult /plus /=. (destruct i as [ | i] ; destruct j as [ | j] ; rewrite /zero /= ; try field) ; (try (destruct i as [ | i]) ; try (destruct j as [ | j]) ; rewrite /zero /one /= ; try field) ; rewrite sum_Sn sum_O /= /plus /= ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Hierarchy PSeries Rbar Lim_seq)