proposition: Lemma Ord3_trichot (a: 'I_3): (a == ord0) (+) (a == ord1_3) (+) (a == ord2_3).
proof: Proof. case:a =>m H. have ->: (Ordinal H == ord0) = (m==0). by apply/eqP/eqP => xx; [ move:(f_equal val xx)| apply:val_inj ]. have ->: (Ordinal H == ord1_3) = (m==1). by apply/eqP/eqP => xx; [ move:(f_equal val xx)| apply:val_inj ]. have ->: (Ordinal H == ord2_3) = (m==2). by apply/eqP/eqP => xx; [ move:(f_equal val xx)| apply:val_inj ]. move: H; rewrite leq_eqVlt eqSS; case/orP; first by move => /eqP -> //. by rewrite !ltnS leqn1; case/orP => /eqP ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)