proposition: Theorem Qnum_inv_Qnat_sub : ∀ j k, (j < k)%nat → Qnum (/ (Qnat k - Qnat j)) = 1%Z.
proof: Proof. intros j k Hjk. rewrite Qnum_inv; [ reflexivity | simpl ]. do 2 rewrite Z.mul_1_r. rewrite Z.add_opp_r. rewrite <- Nat2Z.inj_sub. rewrite <- Nat2Z.inj_0. apply Nat2Z.inj_lt. apply Nat.lt_add_lt_sub_r; assumption. apply Nat.lt_le_incl; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM