proposition: Theorem gcd_ps_add_assoc : ∀ ps₁ ps₂ ps₃ n k, gcd_ps n k ((ps₁ + ps₂) + ps₃)%ps = gcd_ps n k (ps₁ + (ps₂ + ps₃))%ps.
proof: Proof. intros ps₁ ps₂ ps₃ n k. unfold gcd_ps; simpl. unfold ps_ordnum_add; simpl. unfold ps_ordnum_add; simpl. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Z.min_assoc. unfold cm_factor, cm; simpl; unfold cm; simpl. do 6 rewrite Pos2Z.inj_mul. do 3 rewrite Z.mul_assoc. do 3 f_equal. f_equal; [ idtac | rewrite Z.mul_shuffle0; reflexivity ]. f_equal; rewrite Z.mul_shuffle0; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series