proposition: Lemma Gmorph_clos_trans : forall x y, GoM (mat_exp_fast M (S (log2 dim))) x y <-> GoM M! x y.
proof: Proof. split; intros. rewrite Gmorph_iter_le_fast, iter_le_fast_exp2_same, iter_le_spec in H; destruct H as [p]; destruct H. ded (iter_tc _ _ _ _ H0); trivial. ded (eq_dec_midex eq_nat_dec). ded (clos_trans_bpath H0 (@GoM_restricted M)). rewrite length_nats_decr_lt in H1; unfold inclusion in H1. ded (H1 _ _ H); ded (bpath_iter_le H2). rewrite Gmorph_iter_le_fast, iter_le_fast_spec. rewrite iter_le_spec in H3. destruct H3 as [p]; exists p. intuition. ded (exp2_log2 dim). lia. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)