proposition: Lemma if_negb : forall {A} (b: bool) (x y: A), (if negb b then x else y) = (if b then y else x).
proof: Proof. intros; destruct b; simpl; reflexivity. Qed.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Bool.Bool Coq.Classes.Morphisms Fiat.Common.Coq__8_4__8_5__Compat