proposition: Lemma Rseq_alt_involutive : forall An, Rseq_alt (Rseq_alt An) == An.
proof: Proof. intros An n ; unfold Rseq_alt, Rseq_mult, Rseq_pow. rewrite <- Rmult_assoc, <- pow_add ; replace (n + n)%nat with (2 * n)%nat by ring ; rewrite pow_1_even ; apply Rmult_1_l. Qed.
imports: MyRIneq Rsequence_def