Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 authored Nov 22, 2023
1 parent bc1161b commit 897778d
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion theories/two_way.v
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,8 @@ Section DFA2.
Proof.
rewrite /read.
case: (ord2P _) => [||i] _;apply cards_lt1; rewrite ?cardsX ?cards1 ?muln1;
by auto using detL, detC, detR, dfa2_det.
[auto using detL, detC, detR, dfa2_det..|].
exact/detC/dfa2_det.
Qed.

Lemma step_fun x : functional (step M x).
Expand Down

0 comments on commit 897778d

Please sign in to comment.