proposition: Lemma low_sym h1 h2 : (h1 =~ h2) = (h2 =~ h1).
proof: Proof. by rewrite /loweq eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep