proposition: Lemma exclude5 : excluded_arity 5.
proof: Proof. Presentation red. Pcase L0_1: s[1] <= 5. Pcase L1_1: s[2] <= 5. Pcase L2_1: s[3] <= 6. Pcase: s[3] <= 5. Reducible. Pcase: s[4] <= 5. Reducible. Pcase: s[5] > 6. Hubcap $[1,2]<=0 $[3,4]<=(-6) $[5]<=(-4) $. Pcase: s[5] > 5. Hubcap $[1,2]<=0 $[3,4]<=(-7) $[5]<=(-3) $. Reducible. Pcase: s[5] <= 6. Similar to *L2_1[3]. Pcase: s[4] > 5. Hubcap $[1,2]<=0 $[3,4]<=(-6) $[5]<=(-4) $. Hubcap $[1,2]<=0 $[3,4]<=(-5) $[5]<=(-5) $. Pcase: s[5] <= 5. Similar to L1_1[4]. Pcase L1_2: s[3] <= 5. Pcase: s[2] <= 6. Reducible. Pcase: s[4] <= 5. Similar to L1_1[2]. Pcase L2_1: s[4] <= 6. Pcase: s[5] <= 6. Reducible. Hubcap $[1,2]<=(-4) $[3,4]<=(-2) $[5]<=(-4) $. Pcase: s[5] <= 6. Similar to *L2_1[2]. Hubcap $[1,2]<=(-4) $[3,4]<=(-3) $[5]<=(-3) $. Pcase: s[4] <= 5. Similar to *L1_2[4]. Pcase L1_3: s[2] > 6. Pcase: s[5] > 6. Hubcap $[1,2]<=(-3) $[3,4]<=(-4) $[5]<=(-3) $. Hubcap $[1,2]<=(-3) $[3,4]<=(-5) $[5]<=(-2) $. Pcase: s[5] > 6. Similar to *L1_3[4]. Hubcap $[1,2]<=(-2) $[3,4]<=(-6) $[5]<=(-2) $. Pcase: s[2] <= 5. Similar to L0_1[1]. Pcase: s[3] <= 5. Similar to L0_1[2]. Pcase: s[4] <= 5. Similar to L0_1[3]. Pcase: s[5] <= 5. Similar to L0_1[4]. Hubcap $[1,2]<=(-4) $[3,4]<=(-4) $[5]<=(-2) $. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat ssrint) fourcolor(part hubcap present)