proposition: Lemma similar_seq_sym x y: BR_seq x -> BR_seq y -> similar_seq x y -> similar_seq y x.
proof: Proof. move => sx sy h e ep. move: (h e ep) => [n na nb]; exists n => // m ma mb. have ha: realp (Vg y m) by apply:BR_seq_prop. have hb: realp (Vg x m) by apply:BR_seq_prop. by rewrite (BRabs_diff ha hb); apply: nb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)