proposition: Lemma diff_fset0_elem (e : {fset I}) : e != fset0 -> {i : I | i \in e}.
proof: Proof. by case: e => [] [|i l] iH //=; exists i; rewrite inE eqxx. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)