proposition: Lemma Sum_shift_simpl : forall (G : CAbGroup) (f : nat -> G) m n, Sum (S m) (S n) f [=] Sum m n (fun i => f (S i)).
proof: Proof. intros G f m n. symmetry; apply Sum_shift. intro; reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX