proposition: Theorem reduce_cb2 : forall (a b : poly A0 eqA ltM) (Q : list (poly A0 eqA ltM)), reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (s2p A A0 eqA n ltM a) (s2p A A0 eqA n ltM b) -> CombLinear (b :: Q) (s2p A A0 eqA n ltM a).
proof: Proof. Proof using os cs. intros a b; case a; case b; simpl in |- *. intros x c x0 c1 Q H'0. case reduce_inv2 with (1 := cs) (3 := H'0); auto; intros c0 E; elim E; intros d E0; elim E0; intros H'7 H'8; elim H'8; intros H'9 H'10; elim H'10; intros H'11 H'12; clear H'10 H'8 E0 E. apply CombLinear_comp with (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec x (mults (A:=A) multA (n:=n) d c0)); auto. apply CombLinear_pluspf; auto. generalize c H'0; case x; auto. intros a0 l c2 H'. apply CombLinear_id; auto. change (inPolySet A A0 eqA n ltM (pX a0 l) (exist (canonical A0 eqA ltM) (pX a0 l) c2 :: Q)) in |- *. apply incons with (a := a0) (p := l) (P := Q); auto. apply CombLinear_mults1; auto. apply CombLinear_id; auto. apply inskip; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec x0 (mults (A:=A) multA (n:=n) d c0)) (mults (A:=A) multA (n:=n) d c0)); auto. apply pluspf_minuspf_id with (1 := cs); auto. Qed.