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