proposition: Lemma Pos_pow_1_r: forall p : positive, (1^p = 1)%positive.
proof: Proof. intros p. assert (forall q:positive, Pos.iter id 1 q = 1)%positive as H1. { intros q; apply Pos.iter_invariant; tauto. } induction p. - cbn; rewrite IHp, H1; reflexivity. - cbn; rewrite IHp, H1; reflexivity. - reflexivity. Qed.
imports: PArith ZArith Lia