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