add fcard_gt?P lemmas found in fourcolor

2 files changed, 21 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 9fb79a2..b8231ac 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -608,6 +608,26 @@ Proof. by apply: same_connect1 => /=. Qed.
 Lemma same_fconnect1_r x y : fconnect f x y = fconnect f x (f y).
 Proof. by apply: same_connect1r x => /=. Qed.
 
+Lemma fcard_gt0P (a : {pred T}) : 
+  fclosed f a -> reflect (exists x, x \in a) (0 < fcard f a).
+Proof.
+move => clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x.
+exists (froot f x); rewrite inE roots_root /=; last exact: fconnect_sym.
+by rewrite -(closed_connect clfA (connect_root _ x)).
+Qed.
+
+Lemma fcard_gt1P (A : {pred T}) :
+  fclosed f A ->
+  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].
+  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 _ _)).
+Qed.
+
 End orbit_inj.
 Hint Resolve orbit_uniq : core.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 00823f6..05c5547 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -912,6 +912,7 @@ Arguments subsetPn {T A B}.
 Arguments subset_eqP {T A B}.
 Arguments card_uniqP {T s}.
 Arguments card_geqP {T A n}.
+Arguments card_gt0P {T A}.
 Arguments card_gt1P {T A}.
 Arguments card_gt2P {T A}.
 Arguments properP {T A B}.