diff options
| author | Christian Doczkal | 2020-06-26 12:47:52 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-06-26 12:54:27 +0200 |
| commit | 8a4ae574ed75857b9762e06c11589409874ca1a4 (patch) | |
| tree | 3821509593b5dd052a9487f0e8eacdca247b07dc | |
| parent | 3728862662bd0a5b836dfa746921954604d051ec (diff) | |
fix "Nothing to inject" warnings
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index d1376d0..6495ef6 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -621,8 +621,8 @@ Lemma fcard_gt1P (A : {pred T}) : reflect (exists2 x, x \in A & exists2 y, y \in A & ~~ fconnect f x y) (1 < fcard f A). Proof. -move=> clAf; apply: (iffP card_gt1P) => [|[x] [xA [y yA not_xfy]]]. - move=> [x] [y] [/andP [/= rfx xA]] [/andP[/= rfy yA] xDy]. +move=> clAf; apply: (iffP card_gt1P) => [|[x xA [y yA not_xfy]]]. + move=> [x [y [/andP [/= rfx xA] /andP[/= rfy yA] xDy]]]. by exists x; try exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy). exists (froot f x), (froot f y); rewrite !inE !roots_root ?root_connect //=. by split => //; rewrite -(closed_connect clAf (connect_root _ _)). |