proposition: Lemma cmp_aux2_correct : forall m1 e1 m2 e2, valid_mantissa m1 -> valid_mantissa m2 -> cmp_aux2 m1 e1 m2 e2 = Fcmp_aux2 radix (MtoP m1) (EtoZ e1) (MtoP m2) (EtoZ e2).
proof: Proof. intros m1 e1 m2 e2 H1 H2. unfold cmp_aux2, Fcmp_aux2. rewrite exponent_cmp_correct. do 2 rewrite exponent_add_correct. do 2 (rewrite mantissa_digits_correct ; [idtac | assumption]). unfold radix. case (EtoZ e1 + Zpos (count_digits Carrier.radix (MtoP m1)) ?= EtoZ e2 + Zpos (count_digits Carrier.radix (MtoP m2)))%Z ; try apply refl_equal. rewrite exponent_cmp_correct. rewrite exponent_zero_correct. rewrite exponent_sub_correct. case_eq (EtoZ e1 - EtoZ e2)%Z ; intros ; simpl ; unfold cmp_aux1, Fcmp_aux1. now rewrite mantissa_cmp_correct. generalize (mantissa_shl_correct p m1 (exponent_sub e1 e2) H1). rewrite exponent_sub_correct. refine (fun H0 => _ (proj1 (H0 H)) (proj2 (H0 H))). clear H0. intros H3 H4. rewrite mantissa_cmp_correct. rewrite H3. apply refl_equal. exact H4. exact H2. generalize (mantissa_shl_correct p m2 (exponent_neg (exponent_sub e1 e2)) H2). rewrite exponent_neg_correct. rewrite exponent_sub_correct. rewrite H. refine (fun H0 => _ (proj1 (H0 (refl_equal _))) (proj2 (H0 (refl_equal _)))). clear H0. intros H3 H4. rewrite mantissa_cmp_correct. rewrite H3. apply refl_equal. exact H1. exact H4. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig