proposition: Lemma invr1_ltr0_1ltr : forall x, 0 <<! x -> (1 <<! x) = (x^-1 <<! 1).
proof: Proof. move=> x hx; apply/idP/idP => h1. apply: (ltr_Ilcompat_r hx); rewrite divff // ?mulr1 //. by move: hx; rewrite ltr_lerne eq_sym; case/andP. move:(hx); rewrite -invr_ltr=> hIx; apply: (ltr_Ilcompat_r hIx). by rewrite mulr1 mulVf //; move: hx; rewrite ltr_lerne eq_sym; case/andP. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)