Merge pull request #509 from chdoc/card-lemmas

Card lemmas

1 files changed, 20 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 9fb79a2..d1376d0 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.