proposition: Lemma Sum2_comm_scal' : forall a m n (f: forall i, m <= i -> i <= n -> IR), m <= S n -> Sum2 (fun i Hm Hn => a[*]f i Hm Hn) [=] a[*]Sum2 f.
proof: Proof. intros; unfold Sum2 in |- *. eapply eq_transitive_unfolded. 2: apply Sum_comm_scal'. apply Sum_wd'. assumption. intros. elim (le_lt_dec m i); intros; simpl in |- *. elim (le_lt_dec i n); intros; simpl in |- *; algebra. algebra. Qed.
imports: CoRN.reals.CReals1