proposition: Lemma intro_eq x y : (mnmc_lt_seq x y = false) -> (mnmc_lt_seq y x = false) -> mnmc_eq_seq x y.
proof: Proof. rewrite /mnmc_lt_seq /=. rewrite !Rnat_ltE !Rnat_eqE. case Hlt : (_ < _)=>//=; case Hlt' : (_ < _)=>//=; move: Hlt Hlt'. rewrite !ltnNge !negb_false_iff !eqn_leq =>->->/=. elim: x y => [|hx tx Hind]; case=> // hy ty. rewrite /= !Rnat_ltE !Rnat_eqE. case (ltnP (spec_N hx) (spec_N hy)) => //= Hxy; case (ltnP (spec_N hy) (spec_N hx)) => //= Hyx. have Exy : (spec_N hx == spec_N hy). by apply/eqP/anti_leq; rewrite Hyx. rewrite /mnmc_eq_seq /= Rnat_eqE Exy; rewrite eq_sym in Exy; rewrite Exy /=. exact: Hind. 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)