proposition: Theorem reduce_cb1 : forall (a : poly A0 eqA ltM) (b : list (Term A n)) (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) b -> CombLinear (a :: Q) b.
proof: Proof. Proof using os cs. intros a; case a; simpl in |- *. intros x c b Q H'. cut (canonical A0 eqA ltM b); [ intros Op1 | apply canonical_reduce with (1 := cs) (3 := H') ]; auto. case reduce_inv2 with (1 := cs) (3 := H'); auto; (intros c1 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 := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec x (mults (A:=A) multA (n:=n) d c1)); auto. apply CombLinear_minuspf; auto. apply CombLinear_id; auto. generalize c H'; case x; auto. intros c2 H'0; inversion H'0; auto. intros t l c0 H'0; 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 CombLinear_mults1; auto. apply CombLinear_id; auto. apply inskip; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.