fact: Definition get_coord (i : 'I_3) := match val i with | 0 => xcoord | 1 => ycoord | _ => fun=> 1 end.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)