proposition: Lemma p3m_aux : forall i j : nat, p3m (S i) [^]j [=] p3m j[*]p3m i[^]j.
proof: Proof. intros. unfold p3m in |- *. astepl (([1] [/]ThreeNZ) [^] (S i * j):IR). replace (S i * j) with (j + i * j). Step_final (([1] [/]ThreeNZ) [^]j[*] ([1] [/]ThreeNZ) [^] (i * j):IR). reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)