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