proposition: Theorem reduceplus_cb1_lem : forall (a b : list (Term A n)) (Q : list (poly A0 eqA ltM)), reduceplus A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q a b -> forall x : poly A0 eqA ltM, s2p A A0 eqA n ltM x = a -> CombLinear (x :: Q) b.
proof: Proof. Proof using os cs. intros a b Q H'; elim H'; auto. intros x y H'0 x0; case x0; simpl in |- *; auto. intros x1 c H'1. apply CombLinear_comp with (p := x); auto. rewrite <- H'1; auto. generalize c; case x1; auto. intros t l c0; apply CombLinear_id; auto. change (inPolySet A A0 eqA n ltM (pX t l) (exist (canonical A0 eqA ltM) (pX t l) c0 :: Q)) in |- *; auto. apply incons with (a := t) (p := l) (P := Q); auto. apply eqp_imp_canonical with (1 := cs) (p := x1); auto; rewrite H'1; auto. intros x y z; case y; auto. intros H'0 H'1 H'2 x0 H'3. cut (canonical A0 eqA ltM (pO A n)). intros H'4. apply CombLinear_compo with (L1 := mks A A0 eqA n ltM (pO A n) H'4 :: Q); auto. intros q H'5; inversion H'5; auto. apply CombLinear_id; auto. apply inskip; auto. apply canonicalpO; auto. intros a0 l H'0 H'1 H'2 x0 H'3. cut (canonical A0 eqA ltM (pX a0 l)). intros H'4. apply CombLinear_compo with (L1 := mks A A0 eqA n ltM (pX a0 l) H'4 :: Q); auto. intros q H'5; inversion H'5; auto. apply reduce_cb1; auto. rewrite H'3; auto. apply CombLinear_id; auto. apply inskip; auto. apply canonical_reduce with (1 := cs) (3 := H'0); auto. generalize H'3; case x0; simpl in |- *; auto. intros x1 H'4 H'5; elim H'5; auto. Qed.