proposition: Theorem KS_thm_2_4 (lambda : T1) : T1nf lambda -> T1limit lambda -> forall i j, (i < j)%N -> const_path 1 (canon lambda (S j)) (canon lambda (S i)).
proof: Proof. rewrite -hnf_g2h => Hlambda Hlim i j Hij. move: Hlim; rewrite -(h2g_g2hK lambda) -T1limit_ref => Hlim. have H'ij: (i < j)%coq_nat by apply /ltP. generalize (KS_thm_2_4 Hlambda Hlim H'ij). by rewrite /const_path !g2h_canon !h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)