lemma negb_or (a b : bool) : !(a \/ b) <=> !a /\ !b. proof. split. move => not_or. split. case a. move => a_true. simplify. have contrad : a \/ b. left. trivial. trivial. trivial. case b. move => b_true. simplify. have contrad : a \/ b. right. trivial. trivial. trivial. move => and_not. elim and_not => a_false b_false. case (a \/ b). move => or. elim or. trivial. trivial. trivial. qed.