proposition: Lemma eq_nat_dec_bool_true_iff : forall n1 n2, (if eq_nat_dec n1 n2 then true else false) = true <-> n1 = n2.
proof: Proof. intros n1 n2; destruct (eq_nat_dec n1 n2); simpl; intuition; discriminate. 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