proposition: Remark CombLinear_trans_cons_lem : forall (a : list (Term A n)) (R : list (poly A0 eqA ltM)), CombLinear R a -> forall (b : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), R = b :: Q -> CombLinear Q (s2p A A0 eqA n ltM b) -> CombLinear Q a.
proof: Proof. Proof using os minusA invA divA cs A1. intros a R H'; elim H'; 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 (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; auto. 2: apply canonical_mults with (1 := cs); auto. 2: apply inPolySet_imp_canonical with (L := R); auto. 2: apply CombLinear_canonical with (1 := H'2); auto. 2: apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply CombLinear_pluspf; auto. apply CombLinear_mults1; auto. 2: apply H'3 with (b := b); auto. rewrite H'5 in H'1; inversion H'1; auto. rewrite <- H2 in H'6; simpl in H'6; auto. Qed.