proposition: Lemma eq_nat_dec_refl : forall n, eq_nat_dec n n = left (n<>n) (eq_refl n).
proof: Proof. intro. gen (eq_nat_dec n n). destruct s. rewrite (UIP_refl eq_nat_dec e). refl. cong. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)