1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "character/class_pt.ma".
17 (* TRIPLES OF CHARACTER CLASSES *********************************************)
19 lemma not_p_pS: ∀i. P i → P (i + 1) → False.
21 elim (p_inv_gen … Hi) -Hi #hi #Hi
22 elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
23 lapply (injective_plus_l … HSi) -HSi #H
24 elim (not_b_divides_nbr … H) -H //
27 lemma not_p_pSS: ∀i. P i → P (i + 2) → False.
29 elim (p_inv_gen … Hi) -Hi #hi #Hi
30 elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
31 >plus_plus_comm_23 in HSi; #H
32 lapply (injective_plus_l … H) -H #H
33 elim (not_b_divides_nbr … H) -H //
36 lemma not_p_tS: ∀i. P i → T (i + 1) → False.
38 elim (p_inv_gen … Hp) -Hp #hp #Hp
39 elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
40 >exp_n_m_plus_1 in Ht; <associative_times >associative_plus #H
41 elim (not_b_divides_nbr … H) -H //