proposition: Theorem dec_if_dec_eq {A} (x y: A): Dec (x = y) -> {x = y} + {x <> y}.
proof: Proof. intros. inversion H as [D]. unfold decidable in D. assumption. Defined.
imports: ExtLib(RelDec) Coq(Ascii List NArith String ZArith) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Checker) Generators Producer