proposition: Theorem redln_cons_gen : 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 -> incl (addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os c aP) aP) R -> redIn a b (addEnd A A0 eqA n ltM (nf A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os c aP) aP) Q R.
proof: Proof. intros aP R Q a b c H' H'0 H'1 H'2. apply lem_redln_cons_gen with (Q := c :: Q); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)