proposition: Lemma mantissa_sub_correct : forall x y, valid_mantissa x -> valid_mantissa y -> (MtoP y < MtoP x)%positive -> MtoP (mantissa_sub x y) = (MtoP x - MtoP y)%positive /\ valid_mantissa (mantissa_sub x y).
proof: Proof. intros x y (px, Hx) (py, Hy). unfold mantissa_sub, valid_mantissa, MtoP. rewrite BigN.spec_sub. rewrite Hx, Hy. simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec. intros H1 H2. elim (Pos.lt_irrefl py). now rewrite H1 in H2. intros H1 H2. elim (Pos.lt_irrefl py). now apply Pos.lt_trans with px. intros H _. repeat split. now exists (px - py)%positive. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig