proposition: Lemma pow1_squared : forall z, (pow1 z) ^ 2 = 1.
proof: Proof. destruct z; [simpl; ring | | ]; unfold pow1; destruct p; simpl; ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith