proposition: Lemma Fopp2_correct : forall x : float2, Fopp2 x = (- x)%R :>R.
proof: Proof. intros x. unfold float2R, Fopp2. simpl. apply F2R_Zopp. Qed.
imports: Coq(ZArith Reals Lia) Flocq(Raux Defs Float_prop Operations) Gappa_definitions