proposition: Lemma ord_factor3 p n k k': ord_factor_list p n -> ord_factor_boundary p n k -> ord_factor_boundary p n k' -> k = k'.
proof: Proof. move => ofl [lkn llk sgtk] [lkn' llk' sgtk']. move: (proj31 lkn) (proj31 lkn') => ck ck'. case: (cleT_ell ck ck'). - exact. - move => kk'; move : (sgtk _ (cleR ck) (clt_leT kk' lkn')) => lm. case:(limit_nonsucc' (llk' _ kk') lm). - move => kk'; move : (sgtk' _ (cleR ck') (clt_leT kk' lkn)) => lm. case:(limit_nonsucc' (llk _ kk') lm). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)