proposition: Theorem Qden_inv_Qnat_sub : ∀ j k, (j < k)%nat → Qden (/ (Qnat k - Qnat j)) = Pos.of_nat (k - j).
proof: Proof. intros j k Hjk. apply Pos2Z.inj. rewrite Qden_inv. simpl. do 2 rewrite Z.mul_1_r. symmetry. rewrite <- positive_nat_Z; simpl. rewrite Nat2Pos.id. rewrite Nat2Z.inj_sub; [ | apply Nat.lt_le_incl; assumption ]. reflexivity. intros H. apply Nat.sub_0_le in H. apply Nat.nlt_ge in H; contradiction. 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