fact: Definition familiarity_2 (m n:elt):Prop := match m,n with | 1,2=> True | 1,3 => True | 1,4 => True | 1,5 => True | 2,1 => True | 2,5 => True | 3,1 => True | 3,4 => True | 3,5 => True | 4,1 => True | 4,3 => True | 5,1 => True | 5,2 => True | 5,3 => True | _,_ => False end.
imports: AMM11262