proposition: Lemma Sumx_comm_scal' : forall n (a : IR) (f : forall i, i < n -> IR), Sumx (fun i H => a[*]f i H) [=] a[*]Sumx f.
proof: Proof. simple induction n. intros; simpl in |- *; algebra. clear n; intros; simpl in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply ring_dist_unfolded. apply bin_op_wd_unfolded. apply H with (f := fun i l => f i (Nat.lt_lt_succ_r _ _ l)). algebra. Qed.
imports: CoRN.reals.CReals1