proposition: Lemma inductive_invariant:forall m, m<= n -> {B':t| Subset B' town /\ cardinal B' = m /\ forall b'0 b'1, In b'0 B' -> In b'1 B' -> ~(E.eq b'0 b'1) -> knows b'0 b'1}.
proof: Proof. intros m. induction m; intros H_le. exists empty. repeat split. apply subset_empty. intros b'0 b'1 H0 H1; apply False_ind. elim (FM.empty_iff b'0); intros H2 _; apply H2; assumption. assert (H_le0:=le_Sn_le _ _ H_le). destruct (IHm H_le0) as [B' [H3' [H1 H2]]]. rewrite <- H1 in H_le0. destruct (extendible_to_n B' H3' H_le0) as [B [HB1 [HB2 HB3]]]. destruct (property B HB3 HB1) as [d [Hd1 Hd2]]. exists (add d B'); repeat split. apply subset_add_3. apply diff_1 with B; assumption. apply subset_trans with B; assumption. rewrite <- H1. apply add_cardinal_2. intro Hd4. generalize (in_subset Hd4 HB2). apply diff_2 with town; assumption. intros b'0 b'1 H_b'0 H_b'1 H_neq. destruct ((proj1 (FM.add_iff B' d b'0)) H_b'0) as [H3|H3]. apply knows_sym; apply knows_extensional with d; trivial. destruct ((proj1 (FM.add_iff B' d b'1)) H_b'1) as [H4|H4]. apply False_ind; apply H_neq; rewrite <- H3; assumption. apply knows_sym. apply Hd2; apply in_subset with B'; trivial. destruct ((proj1 (FM.add_iff B' d b'1)) H_b'1) as [H4|H4]. apply knows_extensional with d; trivial. apply knows_sym. apply Hd2; apply in_subset with B'; trivial. apply H2; assumption. Qed.
imports: Arith Omega