proposition: Theorem reduceplus_cb2_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 -> canonical A0 eqA ltM a -> forall x : poly A0 eqA ltM, s2p A A0 eqA n ltM x = b -> CombLinear (x :: Q) a.
proof: Proof. Proof using os cs. intros a b Q H'; elim H'; auto. intros x y H'0 H'1 x0 H'2. apply CombLinear_comp with (p := y); auto. rewrite <- H'2; case x0; simpl in |- *; auto. intros x1; case x1; simpl in |- *; auto. intros t l c; apply CombLinear_id; auto. change (inPolySet A A0 eqA n ltM (pX t l) (exist (fun l0 => canonical A0 eqA ltM l0) (pX t l) c :: Q)) in |- *; apply incons; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros x y z H'0 H'1 H'2 H'3 x0 H'4. lapply H'2; [ intros H'5; lapply (H'5 x0); [ intros H'7; clear H'2 | clear H'2 ] | clear H'2 ]; auto. cut (canonical A0 eqA ltM y). intros H'2. lapply (reduce_cb2 (mks A A0 eqA n ltM x H'3) (mks A A0 eqA n ltM y H'2) Q); simpl in |- *; [ intros H'9 | idtac ]; auto. apply CombLinear_trans_cons_lem with (R := mks A A0 eqA n ltM y H'2 :: x0 :: Q) (b := mks A A0 eqA n ltM y H'2); auto. apply CombLinear_incl with (P := mks A A0 eqA n ltM y H'2 :: Q); auto. intros a0 H'6. apply Incl_inp_inPolySet with (P := mks A A0 eqA n ltM y H'2 :: Q); auto. red in |- *; simpl in |- *; auto with datatypes. intros a1 H'8; elim H'8; auto. apply canonical_reduce with (1 := cs) (3 := H'0); auto. apply canonical_reduce with (1 := cs) (3 := H'0); auto. Qed.