proposition: Lemma Mone_seq_not_diag : forall i j : nat, i <> j -> Mone_seq i j = @zero T.
proof: Proof. elim => //= [ | i IHi] j Hij ; destruct j => //=. apply IHi. contradict Hij. by rewrite Hij. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub