proposition: Lemma sub_pr1r a b: T1nf a -> a - b = zero -> a <= b.
proof: Proof. move => nn h; case /orP: (T1le_total a b) => // h1. by move: (sub_pr1 nn h1); rewrite h T1addn0 => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)