proposition: Lemma An_expand_1 : forall An, An_expand An 1 == An.
proof: Proof. intros An n ; unfold An_expand, Rseq_pow, Rseq_mult ; rewrite pow1, Rmult_1_l ; reflexivity. Qed.
imports: Lia MyRIneq Rpow_facts Rsequence_def Rsequence_rewrite_facts Rpser_def