proposition: Lemma Fshift2_correct : forall x y : float2, match Fshift2 x y with | (mx, my, e) => Float2 mx e = x :>R /\ Float2 my e = y :>R end.
proof: Proof. intros (mx, ex) (my, ey). unfold Fshift2. simpl. assert (ex = ex - ey + ey)%Z by ring. pattern ex at - 1 ; rewrite H. destruct (ex - ey)%Z as [|d|d] ; repeat split. rewrite <- (float2_shl_correct mx _ d). now ring_simplify (Zpos d + ey - Zpos d)%Z. rewrite Zplus_comm. apply float2_shl_correct. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions