proposition: Theorem redln_cons : forall (aP R Q : list (poly A0 eqA ltM)) (a b c : poly A0 eqA ltM), In a aP -> In b aP -> redIn a b aP (c :: Q) R -> red A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec c R -> redIn a b aP Q R.
proof: Proof. intros aP R Q a b c H' H'0 H'1 H'2; try assumption. apply lem_redln_cons with (Q := c :: Q) (c := c); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)