proposition: Lemma Gmorph_iter_le_fast : forall n x y, GoM (mat_exp_fast M n) x y <-> iter_le_fast (GoM M) n x y.
proof: Proof. induction n; intros. simpl; auto; tauto. simpl; split; intros. rewrite Gmorph_mult in H. unfold compose in H; destruct H as [z]; destruct H. rewrite Gmorph_plus in H. destruct H. left; unfold compose; exists z; rewrite IHn in *; auto with *. right; unfold GoM in H; rewrite mat_id_spec in H. destruct H; destruct H1; subst; rewrite IHn in H0; auto with *. rewrite Gmorph_mult. unfold compose in *; destruct H. destruct H as [z]; exists z; destruct H. rewrite Gmorph_plus; split; try left; auto; rewrite IHn; auto. exists x; split; rewrite <- IHn in H; auto. gen (GoM_true_bounds H); intros. rewrite Gmorph_plus; right; unfold GoM; rewrite mat_id_spec; intuition; auto with *. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)