proposition: Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y].
proof: Proof. intros x y; rewrite <- spec_mul; auto. unfold mul_norm, mul; destruct x; destruct y. apply Qeq_refl. apply spec_mul_norm_Qz_Qq. rewrite spec_mul_norm_Qz_Qq; qsimpl; ring. rename t0 into nx, t3 into dy, t2 into ny, t1 into dx. destruct (spec_irred nx dy) as (g & Hg). destruct (spec_irred ny dx) as (g' & Hg'). assert (Hz := spec_irred_zero nx dy). assert (Hz':= spec_irred_zero ny dx). destruct irred as (n1,d1); destruct irred as (n2,d2). simpl @snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. rewrite spec_norm_denum. qsimpl. match goal with E : (_ * _ = 0)%Z |- _ => rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end. rewrite Eq in *; simpl in *. rewrite <- Hg2' in *; auto with zarith. rewrite Eq in *; simpl in *. rewrite <- Hg2 in *; auto with zarith. match goal with E : (_ * _ = 0)%Z |- _ => rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end. rewrite Hz' in Eq; rewrite Eq in *; auto with zarith. rewrite Hz in Eq; rewrite Eq in *; auto with zarith. rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig