proposition: Lemma connected_and : forall d1 d2, connected d1 -> connected d2 -> connected (fun t => d1 t /\ d2 t).
proof: Proof. intros d1 d2 H1 H2 u v [D1u D2u] [D1v D2v] t Ht. split. now apply H1 with (3 := Ht). now apply H2 with (3 := Ht). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)