proposition: Theorem CombLinear_reduce : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), reduce A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q p q -> canonical A0 eqA ltM p -> CombLinear Q q -> CombLinear Q p.
proof: Proof. Proof using os cs. intros Q p q H'0 H'1 H'2. case reduce_inv2 with (1 := cs) (3 := H'0); auto. intros x H; elim H; intros a H0; elim H0; intros H1 H2; elim H2; intros H3 H4; elim H4; intros H5 H6; clear H4 H2 H0 H. apply CombLinear_1 with (a := a) (p := q) (q := x); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n). cut (canonical A0 eqA ltM q); [ intros Op1 | apply canonical_reduce with (1 := cs) (3 := H'0) ]; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a x) (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec p (mults (A:=A) multA (n:=n) a x))); 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 p (mults (A:=A) multA (n:=n) a x)) (mults (A:=A) multA (n:=n) a x)); auto. apply pluspf_minuspf_id with (1 := cs); auto. Qed.