proposition: Theorem Falign_spec : forall f1 f2 : float beta, let '(m1, m2, e) := Falign f1 f2 in F2R f1 = @F2R beta (Float m1 e) /\ F2R f2 = @F2R beta (Float m2 e).
proof: Proof. unfold Falign. intros (m1, e1) (m2, e2). generalize (Zle_cases e1 e2). case (Zle_bool e1 e2) ; intros He ; split ; trivial. now rewrite <- F2R_change_exp. rewrite <- F2R_change_exp. apply refl_equal. lia. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop