fact: Fixpoint MFactor (P: Pol) (M: Mon) : Pol * Pol := match P, M with _, mon0 => (Pc cO, P) | Pc _, _ => (P, Pc cO) | Pinj j1 P1, zmon j2 M1 => match (j1 ?= j2) with Eq => let (R,S) := MFactor P1 M1 in (mkPinj j1 R, mkPinj j1 S) | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in (mkPinj j1 R, mkPinj j1 S) | Gt => (P, Pc cO) end | Pinj _ _, vmon _ _ => (P, Pc cO) | PX P1 i Q1, zmon j M1 => let M2 := zmon_pred j M1 in let (R1, S1) := MFactor P1 M in let (R2, S2) := MFactor Q1 M2 in (mkPX R1 i R2, mkPX S1 i S2) | PX P1 i Q1, vmon j M1 => match (i ?= j) with Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in (mkPX R1 i Q1, S1) | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in (mkPX R1 i Q1, S1) | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO)) end end.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory