proposition: Theorem reds_com : forall (P : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), reds a b P -> reds b a P.
proof: Proof. intros P a b H'; elim H'; simpl in |- *; auto. intros P0 a0 b0 H'0. apply reds0; auto. apply red_com; auto. intros P0 a0 b0 c H'0 H'1 H'2 H'3 H'4 H'5. apply reds1 with (c := c); auto. apply divp_ppc; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)