proposition: Theorem Falign_spec_exp: forall f1 f2 : float beta, snd (Falign f1 f2) = Z.min (Fexp f1) (Fexp f2).
proof: Proof. intros (m1,e1) (m2,e2). unfold Falign; simpl. generalize (Zle_cases e1 e2);case (Zle_bool e1 e2); intros He. case (Zmin_spec e1 e2); intros (H1,H2); easy. case (Zmin_spec e1 e2); intros (H1,H2); easy. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop