(* logic-examp2.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.