Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype. Require Import finfun finset. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section arith. (* A few arithmetic lemmas. *) Lemma ex_arith1 : forall k n, 0 < k < n -> 0 < n - k < n. Proof. move => k n /andP [k0 kn]; rewrite subn_gt0 kn /=. by rewrite -{2}[n]subn0 ltn_sub2l // (ltn_trans k0). Qed. Lemma ex_arith2 : forall k n, (0 < k < n) = (0 < n - k < n). Proof. move => k n; apply/idP/idP. by apply: ex_arith1. move/andP => [h1 h2]. apply/andP; split; last by rewrite -subn_gt0. move : h2 {h1}; case : k => //. by rewrite subn0 ltnn. Qed. Lemma ord_to_nat : forall n p (i : 'I_n.+1) (j : 'I_p.+1), i + j < (n + p).+1. move => n p [i il] [j jl] /=. move : il jl; rewrite !ltnS => il jl. by apply: leq_add. Qed. Lemma ord_to_nat2 : forall n (i : 'I_n), i + n < 2 * n. by move => n [i il] /=; rewrite mulSn mul1n ltn_add2r. Qed. End arith. (* simples lemmas about fintype *) Section fintype. Lemma inj_card_le (I J : finType) (f : I -> J) : injective f -> #|I| <= #|J|. Proof. by move=> H; rewrite -(card_codom H); apply: max_card. Qed. Lemma ord1 : forall i : 'I_1, i = ord0. Proof. by case; case=> // i; apply: ord_inj. Qed. End fintype. Section finset. Variable T: finType. (* state and prove that E anf being finite sets : E ∪ F = (E − F) ∪ (E ∩ F) ∪ (F − E). *) (* Lemma unionEF ( E F : {set T}) : E :|: F = (E :\: F) :|: (E :&: F) :|: (F :\: E). apply/setP=>i; rewrite !inE. case : (boolP (i \in E))=>//=; case : (boolP (i \in F))=>//=. Qed.*) (* state and prove that card(E ∪ F) = card E + card F - card(E ∩ F). *) (*Lemma cardU ( E F : {set T}): #|E :|: F| = #|E| + #|F| - #|E :&: F|. by rewrite cardsU cardsI. Qed. *) Lemma adds: forall (a b : T) (E : {set T}), a != b -> a \notin E -> b \notin E -> #| a |: (b |: E)| = #|E| + 2. Proof. move=> a b E Hab Ha Hb. rewrite !cardsU1 Hb. move/eqP:Hab. case : (boolP (a \in b |: E)). rewrite in_setU1. case/orP=> //=. by move/eqP ->. move=> HaT; by rewrite HaT in Ha. by rewrite addnA addnC. Qed. End finset.