proposition: Lemma prl_exa3_prop3 i j: gle r i j -> lf_axiom (csum2^~ (j -c i)) Nat Nat.
proof: Proof. move => leij; move/(proj33 prl_exa3_prop1):leij => [ha hb hc] => x xN. exact: (NS_sum xN (NS_diff _ hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)