proposition: Theorem reduce_cb : forall (a 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 a b -> canonical A0 eqA ltM a -> CombLinear Q a -> CombLinear Q b.
proof: Proof. Proof using os cs. intros a b Q H' H'0 H'1. 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 c 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); auto. apply CombLinear_comp with (p := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec a (mults (A:=A) multA (n:=n) d c)); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.