Commit 67b11a56 authored by MARCHE Claude's avatar MARCHE Claude

fix Coq proof

parent ae9ef936
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem G2 : False.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
Qed.
(* DO NOT EDIT BELOW *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment