proposition: Lemma Sum2_wd : forall m n, m <= S n -> forall f g, (forall i Hm Hn, f i Hm Hn [=] g i Hm Hn) -> Sum2 m n f [=] Sum2 m n g.
proof: Proof. intros m n H f g H0. unfold Sum2 in |- *. apply Sum_wd'. assumption. intros i H1 H2. elim le_lt_dec; intro H3; [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto ]. elim le_lt_dec; intro H4; [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto ]. algebra. Qed.
imports: CoRN.algebra.CAbGroups Coq.Arith.Peano_dec Coq(Lia)