proposition: Lemma negb_eq : forall b, negb b = implb b false.
proof: Proof. destruct b ; simpl; auto. Qed.
imports: Cdcl.Itauto Uint63 Bool ZArith Lia Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia Bool ZifyClasses Coq.ZArith.ZArith Coq.micromega.Lia Classical