proposition: Lemma Nintcc_exten a b c d: a <=c b -> natp b -> Nintcc a b = Nintcc c d -> a = c /\ b = d.
proof: Proof. move => lab bN ss. have aN := NS_le_nat lab bN. have laa:= cleR (proj31 lab). have lbb:= cleR (proj32 lab). have: inc a (Nintcc a b) by apply/Nint_ccP. rewrite ss => /Nint_ccP [ [cN _ lca] [_ dN _]]. have: inc b (Nintcc a b) by apply/Nint_ccP. rewrite ss => /Nint_ccP [ _ [_ _ lbd]]. have lcc := cleR (proj31 lca). have ldd := cleR (proj32 lbd). have lcd := (cleT lca (cleT lab lbd)). have: inc c (Nintcc a b) by rewrite ss; apply/Nint_ccP. move/Nint_ccP => [ [_ _ /(cleA lca) <- ] _]. have: inc d (Nintcc a b) by rewrite ss; apply/Nint_ccP. by move/Nint_ccP => [ _ [_ _ /(cleA lbd) <- ]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)