proposition: Lemma Key_1a : forall (i j : nat) (a t : IR), a[*] (t[*]p3m (S j)) [^]i [=] p3m i[*] (a[*] (t[*]p3m j) [^]i).
proof: Proof. intros. astepl (a0[*] (t[^]i[*]p3m (S j) [^]i)). astepl (a0[*] (t[^]i[*] (p3m i[*]p3m j[^]i))). astepr (p3m i[*] (a0[*] (t[^]i[*]p3m j[^]i))). rational. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)