proposition: Lemma interval_def i j: MoreLists.interval i j = index_iota i (S j).
proof: Proof. by rewrite /index_iota /MoreLists.interval iota_adapt. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)