proposition: Lemma F: False.
proof: Proof. case Hsucc => _ H. move: R1 ;case => x0 Hx0. move: (H x0) => //; move: Hx0. move /andP => // [H' H''] H'''. by move: (H''' H') => // /negP. Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)