proposition: Lemma cpoly_mult_dist_rht : forall p q r, cpoly_mult_cs (cpoly_plus_cs p q) r [=] cpoly_plus_cs (cpoly_mult_cs p r) (cpoly_mult_cs q r).
proof: Proof. intros. apply eq_transitive_unfolded with (cpoly_mult_cs r (cpoly_plus_cs p q)). apply cpoly_mult_commutative. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cs r p) (cpoly_mult_cs r q)). generalize cpoly_cr_dist; intro. unfold distributive in H. simpl in H. simpl in |- *. apply H. apply cpoly_plus_op_wd. apply cpoly_mult_commutative. apply cpoly_mult_commutative. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational