proposition: Lemma ltr_oppgtr : forall x y, (-x <<! -y) = (y <<! x) .
proof: Proof. Proof . move=> x y . rewrite !ltr_lerne ler_oppger; case (y <<= x) => //= . apply congr1; apply/eqP/eqP => [H|->//] . by rewrite -[y]opprK -[x]opprK H . Qed . Lemma lt0r_gtNr0 : forall x, (0 <<! -x) = (x <<! 0) . Proof . by move=> x; rewrite -{1}oppr0 ltr_oppgtr . Qed . Lemma gtr0_ltNr0 : forall x, (0 <<! x) = (- x <<! 0). Proof. by move=> x; rewrite -[x]opprK lt0r_gtNr0 opprK. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)