proposition: Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
proof: Proof. move=> x y; rewrite /lt /mnmc_lt_seq /=; move/orP; elim. { move=> Hlt Heq; move: Heq Hlt; move/mnmc_eq_seqP/eqP->. by rewrite Rnat_E ltnn. } move/andP; case=>_. move=> Hlt /mnmc_eq_seqP/eqP Heq; move: Hlt; rewrite Heq. elim y => [//|h t Hind] /orP [H|H]; [by move: H; rewrite Rnat_E ltnn|]. move/andP in H; apply Hind, H. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)