proposition: Lemma FNth_mult' : forall n, Feq I (F{*}F{^}n) (F{^}S n).
proof: Proof. intro; FEQ. simpl in |- *. eapply eq_transitive_unfolded. 2: apply mult_commutes. apply bin_op_wd_unfolded. rational. change (F x (ProjIR2 Hx) [^]n [=] F x Hx'[^]n) in |- *. apply nexp_wd; rational. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1