proposition: Theorem Cb_trans : forall (a b : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), Cb a (addEnd b Q) -> Cb b Q -> Cb a Q.
proof: Proof. Proof using os minusA invA divA cs A1. intros a b; case a; case b; simpl in |- *; auto. intros x c x0 H' Q H'0 H'1. apply CombLinear_trans1 with (R := addEnd (exist (fun l : list (Term A n) => canonical A0 eqA ltM l) x c) Q) (b := exist (fun l : list (Term A n) => canonical A0 eqA ltM l) x c); auto. Qed.
imports: Buchberger(moreCoefStructure)