proposition: Lemma low_trans h2 h1 h3 : h1 =~ h2 -> h2 =~ h3 -> h1 =~ h3.
proof: Proof. by rewrite /loweq; move/eqP=>->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep