proposition: Lemma defUnr h1 h2 : def (h1 :+ h2) -> def h2.
proof: Proof. by case: h1=>h1 // H; case: h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep