proposition: Lemma idvalue_cprojP r x: equivalence r -> sub x (substrate r) ->forall y, inc y (inverse_direct_value (canon_proj r) x) <-> (inc y (substrate r) /\ (exists2 z, inc z x & class r y = class r z)).
proof: Proof. have ff:= (canon_proj_f r). move => pa pb; move: (pb); rewrite - canon_proj_s => pc y. split. move/(idvalue_P ff pc) => [qa [v qb vx]]; split; first by exact. have ysr: inc y (substrate r) by rewrite - canon_proj_s. by ex_tac; move: vx; rewrite !canon_proj_V //;apply: pb. move => [qa [v qb qc]]; apply/(idvalue_P ff pc). have vsr: inc v (substrate r) by apply: pb. have ysr: inc y (substrate r) by move: qa; aw. by split => //;ex_tac; rewrite !canon_proj_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)