proposition: Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
proof: Proof. move=> x y z; rewrite /lt /mnmc_lt_seq. set x' := _ :: x; set y' := _ :: y; set z' := _ :: z. clearbody x' y' z'; clear x y z; move: x' y' z'. elim => [|hx tx Hind] y z; [by case y => // hy ty; case z|]. case y => // hy ty; case z => // hz tz. move/orP; rewrite !Rnat_E => -[Hxy|Hxy]. { move/orP; rewrite !Rnat_E => -[Hyz|Hyz]; apply/orP; rewrite !Rnat_E; left; [by move: Hyz; apply ltn_trans|]. move/andP in Hyz; destruct Hyz as [Hyz Hyz']. by move/eqP in Hyz; rewrite -Hyz. } move/andP in Hxy; destruct Hxy as [Hxy Hxy']; move/eqP in Hxy. rewrite /mnmc_lt_seq_aux !Rnat_E Hxy. move/orP => [Hyz|Hyz]; apply/orP; [by left|right]. move/andP in Hyz; destruct Hyz as [Hyz Hyz']; rewrite Hyz /=. by move: Hyz'; apply 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)