(* logic-examp.ec *)

require import AllCore.

lemma negb_or (a b : bool) :
  !(a \/ b) <=> !a /\ !b.
proof.

qed.

lemma foo (x y z : int) :
  !(x < y \/ y < z) <=> ! x < y /\ ! y < z.
proof.

qed.

lemma negb_or' (a b : bool) :
  !(a \/ b) <=> !a /\ !b.
proof.

qed.

lemma negb_or'' (a b : bool) :
  !(a \/ b) <=> !a /\ !b.
proof.

qed.

lemma negb_or''' (a b : bool) :
  !(a \/ b) <=> !a /\ !b.
proof.

qed.