proposition: Lemma unAC h1 h2 h3 : h1 :+ h2 :+ h3 = h1 :+ h3 :+ h2.
proof: Proof. by rewrite (unC h1) -unA unC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep