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