proposition: Lemma pneq_dec `{EqDec k} {x y : k} (N : x ≠ y) : { N' | eq_dec x y = right N' }.
proof: Proof. destruct (eq_dec x y); auto. - subst; contradiction. - now exists n. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib