proposition: Lemma gt_inv_1: forall n1 n2 a1 a2, In n1 a1 -> In n2 a2 -> n1 > n2 -> In n1 (fst (gt_inv a1 a2)) /\ In n2 (snd (gt_inv a1 a2)).
proof: Proof. unfold In, gt_inv; intros; cbn. intuition auto; apply Zinf.min_1; auto. apply Zinf.In_mono with ((-n2) - 1). lia. apply Zinf.pred_1; auto. apply Zinf.In_mono with (n1 - 1). lia. apply Zinf.pred_1; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)