proposition: Lemma path_pi3 : path R3 pi3.
proof: Proof. case => [|n] ; rewrite /pi3 /R3 /=. - case e : (f 0); case : (ifP _) => //=; case/existsP; by case. - case e : (f n) => //=. + have -> /= : [exists m : 'I_n.+1, f m]. apply/existsP. by exists ord_max. by case: (ifP _). - case: (ifP _) => //=. + case/existsP => m fm. suff -> : [exists m : 'I_n.+1, f m] by []. apply/existsP. exists (inord m). by rewrite inordK // ltnW // ltnS ltn_ord. + move => H. case: (ifP _) => //; last by case: (ifP _). case/existsP => m fm /=. apply: contraFT H => _. apply/existsP. suff On : m < n by exists (Ordinal On). rewrite ltn_neqAle -ltnS ltn_ord andbT. apply: contraTneq fm => ->. by rewrite e. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)