proposition: Remark CombLinear_trans1 : forall (a : list (Term A n)) (R : list (poly A0 eqA ltM)), CombLinear A A0 eqA plusA multA eqA_dec n ltM ltM_dec R a -> forall (b : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), R = addEnd b Q -> CombLinear A A0 eqA plusA multA eqA_dec n ltM ltM_dec Q (s2p A A0 eqA n ltM b) -> CombLinear A A0 eqA plusA multA eqA_dec n ltM ltM_dec Q a.
proof: Proof. Proof using os minusA invA divA cs A1. intros a R H'; elim H'; auto. intros b Q H'0 H'1. apply CombLinear_0; auto. intros a0 p q s H'0 H'1 H'2 H'3 H'4 b Q H'5 H'6. apply CombLinear_comp with (1 := cs) (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a0 q) p); auto. 2: apply eqp_imp_canonical with (1 := cs) (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a0 q) p); auto. 2: apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. 2: apply canonical_pluspf with (1 := os); auto. 2: apply canonical_mults with (1 := cs); auto. 2: apply inPolySet_imp_canonical with (L := R); auto. 2: apply CombLinear_canonical with (eqA_dec := eqA_dec) (ltM_dec := ltM_dec) (1 := cs) (Q := R); auto. 2: apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply CombLinear_pluspf with (1 := cs); auto. apply CombLinear_mults1 with (1 := cs); auto. 2: apply H'3 with (b := b); auto. case (inPolySet_addEnd q b Q); auto. rewrite <- H'5; auto. intros H'7; rewrite H'7; auto. intros; (apply CombLinear_id with (1 := cs); auto). Qed.
imports: Buchberger(moreCoefStructure)